$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $x$:$A$, $v$:$B$($x$), ${\it eqa}$:EqDecider($A$). $x$ : $v$ $\subseteq$ $x$ : $v$